YES 2.05 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((lookup :: Eq a => [a ->  [([a],b)]  ->  Maybe b) :: Eq a => [a ->  [([a],b)]  ->  Maybe b)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((lookup :: Eq a => [a ->  [([a],b)]  ->  Maybe b) :: Eq a => [a ->  [([a],b)]  ->  Maybe b)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
lookup k [] = Nothing
lookup k ((x,y: xys)
 | k == x
 = Just y
 | otherwise
 = lookup k xys

is transformed to
lookup k [] = lookup3 k []
lookup k ((x,y: xys) = lookup2 k ((x,y: xys)

lookup0 k x y xys True = lookup k xys

lookup1 k x y xys True = Just y
lookup1 k x y xys False = lookup0 k x y xys otherwise

lookup2 k ((x,y: xys) = lookup1 k x y xys (k == x)

lookup3 k [] = Nothing
lookup3 xy xz = lookup2 xy xz



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (lookup :: Eq b => [b ->  [([b],a)]  ->  Maybe a)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yu3400), Succ(yu40001000)) → new_primPlusNat(yu3400, yu40001000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yu30100), Succ(yu4000100)) → new_primMulNat(yu30100, Succ(yu4000100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(yu3000), Succ(yu400000)) → new_primEqNat(yu3000, yu400000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs0(Right(yu300), Right(yu40000), de, app(app(ty_@2, eb), ec)) → new_esEs2(yu300, yu40000, eb, ec)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs3(yu302, yu40002, bdb, bdc, bdd)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(app(ty_@2, he), hf)) → new_esEs2(yu301, yu40001, he, hf)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(ty_Maybe, ha)) → new_esEs(yu301, yu40001, ha)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(ty_Maybe, fh), fb) → new_esEs(yu300, yu40000, fh)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(ty_Maybe, bab), fd, ff) → new_esEs(yu300, yu40000, bab)
new_esEs(Just(yu300), Just(yu40000), app(app(app(ty_@3, bg), bh), ca)) → new_esEs3(yu300, yu40000, bg, bh, ca)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(ty_[], bcg)) → new_esEs1(yu302, yu40002, bcg)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), fg) → new_esEs1(yu311, yu40011, fg)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(app(ty_@2, gd), ge), fb) → new_esEs2(yu300, yu40000, gd, ge)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(ty_[], eh)) → new_esEs1(yu310, yu40010, eh)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(app(app(ty_@3, hg), hh), baa)) → new_esEs3(yu301, yu40001, hg, hh, baa)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(ty_[], bbf), ff) → new_esEs1(yu301, yu40001, bbf)
new_esEs0(Left(yu300), Left(yu40000), app(app(app(ty_@3, db), dc), dd), cc) → new_esEs3(yu300, yu40000, db, dc, dd)
new_esEs(Just(yu300), Just(yu40000), app(ty_Maybe, ba)) → new_esEs(yu300, yu40000, ba)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(app(ty_Either, hb), hc)) → new_esEs0(yu301, yu40001, hb, hc)
new_esEs0(Left(yu300), Left(yu40000), app(app(ty_Either, cd), ce), cc) → new_esEs0(yu300, yu40000, cd, ce)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(ty_Maybe, bbc), ff) → new_esEs(yu301, yu40001, bbc)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(ty_[], gc), fb) → new_esEs1(yu300, yu40000, gc)
new_esEs0(Left(yu300), Left(yu40000), app(app(ty_@2, cg), da), cc) → new_esEs2(yu300, yu40000, cg, da)
new_esEs0(Right(yu300), Right(yu40000), de, app(app(app(ty_@3, ed), ee), ef)) → new_esEs3(yu300, yu40000, ed, ee, ef)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(ty_Maybe, bcd)) → new_esEs(yu302, yu40002, bcd)
new_esEs0(Right(yu300), Right(yu40000), de, app(app(ty_Either, dg), dh)) → new_esEs0(yu300, yu40000, dg, dh)
new_esEs(Just(yu300), Just(yu40000), app(app(ty_Either, bb), bc)) → new_esEs0(yu300, yu40000, bb, bc)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(app(app(ty_@3, bca), bcb), bcc), ff) → new_esEs3(yu301, yu40001, bca, bcb, bcc)
new_esEs(Just(yu300), Just(yu40000), app(app(ty_@2, be), bf)) → new_esEs2(yu300, yu40000, be, bf)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(app(ty_Either, de), cc)) → new_esEs0(yu310, yu40010, de, cc)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(app(ty_@2, bch), bda)) → new_esEs2(yu302, yu40002, bch, bda)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(ty_@2, baf), bag), fd, ff) → new_esEs2(yu300, yu40000, baf, bag)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(app(ty_@2, bbg), bbh), ff) → new_esEs2(yu301, yu40001, bbg, bbh)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(ty_Maybe, eg)) → new_esEs(yu310, yu40010, eg)
new_esEs0(Right(yu300), Right(yu40000), de, app(ty_[], ea)) → new_esEs1(yu300, yu40000, ea)
new_esEs(Just(yu300), Just(yu40000), app(ty_[], bd)) → new_esEs1(yu300, yu40000, bd)
new_esEs0(Left(yu300), Left(yu40000), app(ty_[], cf), cc) → new_esEs1(yu300, yu40000, cf)
new_esEs0(Right(yu300), Right(yu40000), de, app(ty_Maybe, df)) → new_esEs(yu300, yu40000, df)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(app(app(ty_@3, fc), fd), ff)) → new_esEs3(yu310, yu40010, fc, fd, ff)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(app(ty_@2, fa), fb)) → new_esEs2(yu310, yu40010, fa, fb)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(ty_[], bae), fd, ff) → new_esEs1(yu300, yu40000, bae)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(app(ty_Either, ga), gb), fb) → new_esEs0(yu300, yu40000, ga, gb)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(ty_[], hd)) → new_esEs1(yu301, yu40001, hd)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(app(ty_Either, bbd), bbe), ff) → new_esEs0(yu301, yu40001, bbd, bbe)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(app(ty_Either, bce), bcf)) → new_esEs0(yu302, yu40002, bce, bcf)
new_esEs0(Left(yu300), Left(yu40000), app(ty_Maybe, cb), cc) → new_esEs(yu300, yu40000, cb)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(app(ty_@3, bah), bba), bbb), fd, ff) → new_esEs3(yu300, yu40000, bah, bba, bbb)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(app(app(ty_@3, gf), gg), gh), fb) → new_esEs3(yu300, yu40000, gf, gg, gh)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(ty_Either, bac), bad), fd, ff) → new_esEs0(yu300, yu40000, bac, bad)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup(:(yu30, yu31), :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup1(yu30, yu31, yu4000, yu4001, yu401, yu41, new_asAs(new_esEs4(yu30, yu4000, bd), new_esEs5(yu31, yu4001, bd)), bc, bd)
new_lookup(:(yu30, yu31), :(@2([], yu401), yu41), bc, bd) → new_lookup(:(yu30, yu31), yu41, bc, bd)
new_lookup1(yu13, yu14, yu15, yu16, yu17, yu18, False, ba, bb) → new_lookup(:(yu13, yu14), yu18, ba, bb)
new_lookup([], :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup([], yu41, bc, bd)

The TRS R consists of the following rules:

new_esEs9(Left(yu300), Left(yu40000), ty_@0, bg) → new_esEs7(yu300, yu40000)
new_primPlusNat1(Succ(yu3400), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu3400, yu40001000)))
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Ordering) → new_esEs11(yu301, yu40001)
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_esEs21(yu302, yu40002, ty_Integer) → new_esEs15(yu302, yu40002)
new_esEs4(yu30, yu4000, app(app(app(ty_@3, cc), cd), ce)) → new_esEs13(yu30, yu4000, cc, cd, ce)
new_esEs5([], [], bd) → True
new_esEs21(yu302, yu40002, ty_Ordering) → new_esEs11(yu302, yu40002)
new_esEs20(yu301, yu40001, ty_Bool) → new_esEs10(yu301, yu40001)
new_esEs9(Left(yu300), Left(yu40000), ty_Bool, bg) → new_esEs10(yu300, yu40000)
new_esEs11(EQ, EQ) → True
new_esEs23(yu300, yu40000, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs14(yu300, yu40000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs19(yu300, yu40000, app(ty_Ratio, hh)) → new_esEs18(yu300, yu40000, hh)
new_esEs18(:%(yu300, yu301), :%(yu40000, yu40001), cf) → new_asAs(new_esEs25(yu300, yu40000, cf), new_esEs26(yu301, yu40001, cf))
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs21(yu302, yu40002, app(ty_[], bbf)) → new_esEs5(yu302, yu40002, bbf)
new_esEs20(yu301, yu40001, ty_Ordering) → new_esEs11(yu301, yu40001)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_[], ee)) → new_esEs5(yu300, yu40000, ee)
new_esEs4(yu30, yu4000, app(ty_Ratio, cf)) → new_esEs18(yu30, yu4000, cf)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(ty_Either, ec), ed)) → new_esEs9(yu300, yu40000, ec, ed)
new_esEs5([], :(yu40010, yu40011), bd) → False
new_esEs5(:(yu310, yu311), [], bd) → False
new_esEs4(yu30, yu4000, app(ty_Maybe, be)) → new_esEs6(yu30, yu4000, be)
new_esEs9(Left(yu300), Left(yu40000), app(ty_Maybe, cg), bg) → new_esEs6(yu300, yu40000, cg)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs7(yu300, yu40000)
new_esEs11(GT, LT) → False
new_esEs11(LT, GT) → False
new_esEs20(yu301, yu40001, ty_Char) → new_esEs14(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(ty_@2, bda), bdb)) → new_esEs12(yu300, yu40000, bda, bdb)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs25(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs9(Left(yu300), Left(yu40000), ty_Char, bg) → new_esEs14(yu300, yu40000)
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_esEs9(Left(yu300), Left(yu40000), ty_Ordering, bg) → new_esEs11(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Float) → new_esEs17(yu301, yu40001)
new_esEs11(EQ, LT) → False
new_esEs11(LT, EQ) → False
new_esEs8(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs16(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs22(yu310, yu40010, ty_Bool) → new_esEs10(yu310, yu40010)
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), cc, cd, ce) → new_asAs(new_esEs19(yu300, yu40000, cc), new_asAs(new_esEs20(yu301, yu40001, cd), new_esEs21(yu302, yu40002, ce)))
new_esEs22(yu310, yu40010, app(ty_Maybe, be)) → new_esEs6(yu310, yu40010, be)
new_esEs15(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs11(yu30, yu4000)
new_esEs20(yu301, yu40001, app(app(ty_@2, bae), baf)) → new_esEs12(yu301, yu40001, bae, baf)
new_esEs4(yu30, yu4000, ty_Float) → new_esEs17(yu30, yu4000)
new_esEs10(True, True) → True
new_esEs20(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs22(yu310, yu40010, app(ty_Ratio, cf)) → new_esEs18(yu310, yu40010, cf)
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs22(yu310, yu40010, ty_Float) → new_esEs17(yu310, yu40010)
new_esEs4(yu30, yu4000, app(ty_[], bh)) → new_esEs5(yu30, yu4000, bh)
new_esEs20(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(ty_Either, bcf), bcg)) → new_esEs9(yu300, yu40000, bcf, bcg)
new_esEs22(yu310, yu40010, app(app(ty_Either, bf), bg)) → new_esEs9(yu310, yu40010, bf, bg)
new_esEs20(yu301, yu40001, app(ty_[], bad)) → new_esEs5(yu301, yu40001, bad)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs23(yu300, yu40000, app(ty_Ratio, bdf)) → new_esEs18(yu300, yu40000, bdf)
new_esEs19(yu300, yu40000, app(app(ty_@2, hc), hd)) → new_esEs12(yu300, yu40000, hc, hd)
new_esEs20(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_esEs26(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs19(yu300, yu40000, app(ty_Maybe, gg)) → new_esEs6(yu300, yu40000, gg)
new_esEs23(yu300, yu40000, app(ty_[], bch)) → new_esEs5(yu300, yu40000, bch)
new_esEs21(yu302, yu40002, app(app(app(ty_@3, bca), bcb), bcc)) → new_esEs13(yu302, yu40002, bca, bcb, bcc)
new_esEs25(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(ty_@2, ef), eg)) → new_esEs12(yu300, yu40000, ef, eg)
new_esEs21(yu302, yu40002, app(app(ty_@2, bbg), bbh)) → new_esEs12(yu302, yu40002, bbg, bbh)
new_esEs20(yu301, yu40001, app(ty_Ratio, bbb)) → new_esEs18(yu301, yu40001, bbb)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, gc), gd), ge)) → new_esEs13(yu300, yu40000, gc, gd, ge)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], fh)) → new_esEs5(yu300, yu40000, fh)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(app(ty_@3, eh), fa), fb)) → new_esEs13(yu300, yu40000, eh, fa, fb)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs22(yu310, yu40010, app(ty_[], bh)) → new_esEs5(yu310, yu40010, bh)
new_esEs20(yu301, yu40001, app(app(ty_Either, bab), bac)) → new_esEs9(yu301, yu40001, bab, bac)
new_esEs9(Left(yu300), Left(yu40000), app(ty_[], dc), bg) → new_esEs5(yu300, yu40000, dc)
new_esEs19(yu300, yu40000, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs24(yu301, yu40001, app(app(ty_@2, bec), bed)) → new_esEs12(yu301, yu40001, bec, bed)
new_esEs11(GT, GT) → True
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs20(yu301, yu40001, app(ty_Maybe, baa)) → new_esEs6(yu301, yu40001, baa)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs15(yu300, yu40000)
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_asAs(False, yu33) → False
new_esEs19(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_primEqNat0(Zero, Zero) → True
new_esEs19(yu300, yu40000, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_Maybe, eb)) → new_esEs6(yu300, yu40000, eb)
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_esEs19(yu300, yu40000, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, fd)) → new_esEs6(yu300, yu40000, fd)
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs10(yu30, yu4000)
new_esEs21(yu302, yu40002, ty_Int) → new_esEs16(yu302, yu40002)
new_esEs19(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs13(yu300, yu40000, bdc, bdd, bde)
new_esEs22(yu310, yu40010, app(app(app(ty_@3, cc), cd), ce)) → new_esEs13(yu310, yu40010, cc, cd, ce)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs16(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), app(app(ty_Either, da), db), bg) → new_esEs9(yu300, yu40000, da, db)
new_esEs23(yu300, yu40000, app(ty_Maybe, bce)) → new_esEs6(yu300, yu40000, bce)
new_esEs19(yu300, yu40000, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs21(yu302, yu40002, ty_@0) → new_esEs7(yu302, yu40002)
new_esEs24(yu301, yu40001, app(ty_[], beb)) → new_esEs5(yu301, yu40001, beb)
new_esEs22(yu310, yu40010, ty_@0) → new_esEs7(yu310, yu40010)
new_primPlusNat0(Succ(yu340), yu4000100) → Succ(Succ(new_primPlusNat1(yu340, yu4000100)))
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs20(yu301, yu40001, ty_Double) → new_esEs8(yu301, yu40001)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, ff), fg)) → new_esEs9(yu300, yu40000, ff, fg)
new_esEs19(yu300, yu40000, app(app(app(ty_@3, he), hf), hg)) → new_esEs13(yu300, yu40000, he, hf, hg)
new_esEs14(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs19(yu300, yu40000, app(app(ty_Either, gh), ha)) → new_esEs9(yu300, yu40000, gh, ha)
new_esEs22(yu310, yu40010, ty_Char) → new_esEs14(yu310, yu40010)
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu301, yu40001, ty_Double) → new_esEs8(yu301, yu40001)
new_esEs20(yu301, yu40001, ty_Float) → new_esEs17(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs8(yu30, yu4000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs9(Left(yu300), Left(yu40000), ty_Float, bg) → new_esEs17(yu300, yu40000)
new_primPlusNat1(Succ(yu3400), Zero) → Succ(yu3400)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs16(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), ty_Double, bg) → new_esEs8(yu300, yu40000)
new_esEs4(yu30, yu4000, app(app(ty_@2, ca), cb)) → new_esEs12(yu30, yu4000, ca, cb)
new_esEs4(yu30, yu4000, app(app(ty_Either, bf), bg)) → new_esEs9(yu30, yu4000, bf, bg)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs24(yu301, yu40001, ty_Bool) → new_esEs10(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs15(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), ty_Integer, bg) → new_esEs15(yu300, yu40000)
new_esEs24(yu301, yu40001, app(app(app(ty_@3, bee), bef), beg)) → new_esEs13(yu301, yu40001, bee, bef, beg)
new_esEs21(yu302, yu40002, ty_Double) → new_esEs8(yu302, yu40002)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Integer) → new_esEs15(yu300, yu40000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_esEs9(Left(yu300), Left(yu40000), ty_Int, bg) → new_esEs16(yu300, yu40000)
new_esEs20(yu301, yu40001, app(app(app(ty_@3, bag), bah), bba)) → new_esEs13(yu301, yu40001, bag, bah, bba)
new_esEs17(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs16(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs19(yu300, yu40000, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs22(yu310, yu40010, ty_Integer) → new_esEs15(yu310, yu40010)
new_esEs10(False, False) → True
new_esEs21(yu302, yu40002, ty_Float) → new_esEs17(yu302, yu40002)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs19(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs22(yu310, yu40010, app(app(ty_@2, ca), cb)) → new_esEs12(yu310, yu40010, ca, cb)
new_asAs(True, yu33) → yu33
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs17(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs8(yu300, yu40000)
new_esEs11(LT, LT) → True
new_esEs4(yu30, yu4000, ty_@0) → new_esEs7(yu30, yu4000)
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs24(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs22(yu310, yu40010, ty_Double) → new_esEs8(yu310, yu40010)
new_esEs6(Nothing, Nothing, be) → True
new_esEs21(yu302, yu40002, ty_Char) → new_esEs14(yu302, yu40002)
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs9(Left(yu300), Left(yu40000), app(app(app(ty_@3, df), dg), dh), bg) → new_esEs13(yu300, yu40000, df, dg, dh)
new_esEs21(yu302, yu40002, app(ty_Maybe, bbc)) → new_esEs6(yu302, yu40002, bbc)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, ga), gb)) → new_esEs12(yu300, yu40000, ga, gb)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs26(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs24(yu301, yu40001, ty_Char) → new_esEs14(yu301, yu40001)
new_esEs6(Nothing, Just(yu40000), be) → False
new_esEs6(Just(yu300), Nothing, be) → False
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs11(GT, EQ) → False
new_esEs11(EQ, GT) → False
new_esEs24(yu301, yu40001, app(ty_Maybe, bdg)) → new_esEs6(yu301, yu40001, bdg)
new_esEs9(Left(yu300), Left(yu40000), app(ty_Ratio, ea), bg) → new_esEs18(yu300, yu40000, ea)
new_esEs21(yu302, yu40002, ty_Bool) → new_esEs10(yu302, yu40002)
new_esEs24(yu301, yu40001, app(ty_Ratio, beh)) → new_esEs18(yu301, yu40001, beh)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_Ratio, fc)) → new_esEs18(yu300, yu40000, fc)
new_esEs7(@0, @0) → True
new_esEs21(yu302, yu40002, app(app(ty_Either, bbd), bbe)) → new_esEs9(yu302, yu40002, bbd, bbe)
new_esEs12(@2(yu300, yu301), @2(yu40000, yu40001), ca, cb) → new_asAs(new_esEs23(yu300, yu40000, ca), new_esEs24(yu301, yu40001, cb))
new_esEs9(Left(yu300), Left(yu40000), app(app(ty_@2, dd), de), bg) → new_esEs12(yu300, yu40000, dd, de)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs14(yu30, yu4000)
new_esEs19(yu300, yu40000, app(ty_[], hb)) → new_esEs5(yu300, yu40000, hb)
new_esEs24(yu301, yu40001, app(app(ty_Either, bdh), bea)) → new_esEs9(yu301, yu40001, bdh, bea)
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_esEs22(yu310, yu40010, ty_Ordering) → new_esEs11(yu310, yu40010)
new_esEs9(Right(yu300), Left(yu40000), bf, bg) → False
new_esEs9(Left(yu300), Right(yu40000), bf, bg) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs21(yu302, yu40002, app(ty_Ratio, bcd)) → new_esEs18(yu302, yu40002, bcd)
new_esEs22(yu310, yu40010, ty_Int) → new_esEs16(yu310, yu40010)
new_esEs5(:(yu310, yu311), :(yu40010, yu40011), bd) → new_asAs(new_esEs22(yu310, yu40010, bd), new_esEs5(yu311, yu40011, bd))
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, gf)) → new_esEs18(yu300, yu40000, gf)

The set Q consists of the following terms:

new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Int)
new_esEs6(Just(x0), Nothing, x1)
new_esEs21(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs7(@0, @0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_[], x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Char)
new_esEs6(Nothing, Nothing, x0)
new_esEs25(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5([], [], x0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_asAs(True, x0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs5([], :(x0, x1), x2)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs19(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Ordering)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs21(x0, x1, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_esEs4(x0, x1, ty_Float)
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_esEs19(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs10(False, False)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs15(Integer(x0), Integer(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_asAs(False, x0)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs22(x0, x1, ty_Double)
new_esEs11(GT, GT)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_sr(Pos(x0), Pos(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs14(Char(x0), Char(x1))
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Ordering)
new_esEs11(LT, GT)
new_esEs11(GT, LT)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Double)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Float)
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(LT, LT)
new_esEs21(x0, x1, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Bool)
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Float)
new_primPlusNat1(Zero, Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs26(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs10(True, True)
new_esEs16(x0, x1)
new_esEs5(:(x0, x1), [], x2)
new_esEs22(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(EQ, EQ)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs24(x0, x1, app(ty_Maybe, x2))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
QDP
                      ↳ UsableRulesProof
                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_lookup([], :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup([], yu41, bc, bd)

The TRS R consists of the following rules:

new_esEs9(Left(yu300), Left(yu40000), ty_@0, bg) → new_esEs7(yu300, yu40000)
new_primPlusNat1(Succ(yu3400), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu3400, yu40001000)))
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Ordering) → new_esEs11(yu301, yu40001)
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_esEs21(yu302, yu40002, ty_Integer) → new_esEs15(yu302, yu40002)
new_esEs4(yu30, yu4000, app(app(app(ty_@3, cc), cd), ce)) → new_esEs13(yu30, yu4000, cc, cd, ce)
new_esEs5([], [], bd) → True
new_esEs21(yu302, yu40002, ty_Ordering) → new_esEs11(yu302, yu40002)
new_esEs20(yu301, yu40001, ty_Bool) → new_esEs10(yu301, yu40001)
new_esEs9(Left(yu300), Left(yu40000), ty_Bool, bg) → new_esEs10(yu300, yu40000)
new_esEs11(EQ, EQ) → True
new_esEs23(yu300, yu40000, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs14(yu300, yu40000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs19(yu300, yu40000, app(ty_Ratio, hh)) → new_esEs18(yu300, yu40000, hh)
new_esEs18(:%(yu300, yu301), :%(yu40000, yu40001), cf) → new_asAs(new_esEs25(yu300, yu40000, cf), new_esEs26(yu301, yu40001, cf))
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs21(yu302, yu40002, app(ty_[], bbf)) → new_esEs5(yu302, yu40002, bbf)
new_esEs20(yu301, yu40001, ty_Ordering) → new_esEs11(yu301, yu40001)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_[], ee)) → new_esEs5(yu300, yu40000, ee)
new_esEs4(yu30, yu4000, app(ty_Ratio, cf)) → new_esEs18(yu30, yu4000, cf)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(ty_Either, ec), ed)) → new_esEs9(yu300, yu40000, ec, ed)
new_esEs5([], :(yu40010, yu40011), bd) → False
new_esEs5(:(yu310, yu311), [], bd) → False
new_esEs4(yu30, yu4000, app(ty_Maybe, be)) → new_esEs6(yu30, yu4000, be)
new_esEs9(Left(yu300), Left(yu40000), app(ty_Maybe, cg), bg) → new_esEs6(yu300, yu40000, cg)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs7(yu300, yu40000)
new_esEs11(GT, LT) → False
new_esEs11(LT, GT) → False
new_esEs20(yu301, yu40001, ty_Char) → new_esEs14(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(ty_@2, bda), bdb)) → new_esEs12(yu300, yu40000, bda, bdb)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs25(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs9(Left(yu300), Left(yu40000), ty_Char, bg) → new_esEs14(yu300, yu40000)
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_esEs9(Left(yu300), Left(yu40000), ty_Ordering, bg) → new_esEs11(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Float) → new_esEs17(yu301, yu40001)
new_esEs11(EQ, LT) → False
new_esEs11(LT, EQ) → False
new_esEs8(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs16(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs22(yu310, yu40010, ty_Bool) → new_esEs10(yu310, yu40010)
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), cc, cd, ce) → new_asAs(new_esEs19(yu300, yu40000, cc), new_asAs(new_esEs20(yu301, yu40001, cd), new_esEs21(yu302, yu40002, ce)))
new_esEs22(yu310, yu40010, app(ty_Maybe, be)) → new_esEs6(yu310, yu40010, be)
new_esEs15(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs11(yu30, yu4000)
new_esEs20(yu301, yu40001, app(app(ty_@2, bae), baf)) → new_esEs12(yu301, yu40001, bae, baf)
new_esEs4(yu30, yu4000, ty_Float) → new_esEs17(yu30, yu4000)
new_esEs10(True, True) → True
new_esEs20(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs22(yu310, yu40010, app(ty_Ratio, cf)) → new_esEs18(yu310, yu40010, cf)
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs22(yu310, yu40010, ty_Float) → new_esEs17(yu310, yu40010)
new_esEs4(yu30, yu4000, app(ty_[], bh)) → new_esEs5(yu30, yu4000, bh)
new_esEs20(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(ty_Either, bcf), bcg)) → new_esEs9(yu300, yu40000, bcf, bcg)
new_esEs22(yu310, yu40010, app(app(ty_Either, bf), bg)) → new_esEs9(yu310, yu40010, bf, bg)
new_esEs20(yu301, yu40001, app(ty_[], bad)) → new_esEs5(yu301, yu40001, bad)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs23(yu300, yu40000, app(ty_Ratio, bdf)) → new_esEs18(yu300, yu40000, bdf)
new_esEs19(yu300, yu40000, app(app(ty_@2, hc), hd)) → new_esEs12(yu300, yu40000, hc, hd)
new_esEs20(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_esEs26(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs19(yu300, yu40000, app(ty_Maybe, gg)) → new_esEs6(yu300, yu40000, gg)
new_esEs23(yu300, yu40000, app(ty_[], bch)) → new_esEs5(yu300, yu40000, bch)
new_esEs21(yu302, yu40002, app(app(app(ty_@3, bca), bcb), bcc)) → new_esEs13(yu302, yu40002, bca, bcb, bcc)
new_esEs25(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(ty_@2, ef), eg)) → new_esEs12(yu300, yu40000, ef, eg)
new_esEs21(yu302, yu40002, app(app(ty_@2, bbg), bbh)) → new_esEs12(yu302, yu40002, bbg, bbh)
new_esEs20(yu301, yu40001, app(ty_Ratio, bbb)) → new_esEs18(yu301, yu40001, bbb)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, gc), gd), ge)) → new_esEs13(yu300, yu40000, gc, gd, ge)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], fh)) → new_esEs5(yu300, yu40000, fh)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(app(ty_@3, eh), fa), fb)) → new_esEs13(yu300, yu40000, eh, fa, fb)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs22(yu310, yu40010, app(ty_[], bh)) → new_esEs5(yu310, yu40010, bh)
new_esEs20(yu301, yu40001, app(app(ty_Either, bab), bac)) → new_esEs9(yu301, yu40001, bab, bac)
new_esEs9(Left(yu300), Left(yu40000), app(ty_[], dc), bg) → new_esEs5(yu300, yu40000, dc)
new_esEs19(yu300, yu40000, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs24(yu301, yu40001, app(app(ty_@2, bec), bed)) → new_esEs12(yu301, yu40001, bec, bed)
new_esEs11(GT, GT) → True
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs20(yu301, yu40001, app(ty_Maybe, baa)) → new_esEs6(yu301, yu40001, baa)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs15(yu300, yu40000)
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_asAs(False, yu33) → False
new_esEs19(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_primEqNat0(Zero, Zero) → True
new_esEs19(yu300, yu40000, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_Maybe, eb)) → new_esEs6(yu300, yu40000, eb)
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_esEs19(yu300, yu40000, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, fd)) → new_esEs6(yu300, yu40000, fd)
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs10(yu30, yu4000)
new_esEs21(yu302, yu40002, ty_Int) → new_esEs16(yu302, yu40002)
new_esEs19(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs13(yu300, yu40000, bdc, bdd, bde)
new_esEs22(yu310, yu40010, app(app(app(ty_@3, cc), cd), ce)) → new_esEs13(yu310, yu40010, cc, cd, ce)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs16(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), app(app(ty_Either, da), db), bg) → new_esEs9(yu300, yu40000, da, db)
new_esEs23(yu300, yu40000, app(ty_Maybe, bce)) → new_esEs6(yu300, yu40000, bce)
new_esEs19(yu300, yu40000, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs21(yu302, yu40002, ty_@0) → new_esEs7(yu302, yu40002)
new_esEs24(yu301, yu40001, app(ty_[], beb)) → new_esEs5(yu301, yu40001, beb)
new_esEs22(yu310, yu40010, ty_@0) → new_esEs7(yu310, yu40010)
new_primPlusNat0(Succ(yu340), yu4000100) → Succ(Succ(new_primPlusNat1(yu340, yu4000100)))
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs20(yu301, yu40001, ty_Double) → new_esEs8(yu301, yu40001)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, ff), fg)) → new_esEs9(yu300, yu40000, ff, fg)
new_esEs19(yu300, yu40000, app(app(app(ty_@3, he), hf), hg)) → new_esEs13(yu300, yu40000, he, hf, hg)
new_esEs14(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs19(yu300, yu40000, app(app(ty_Either, gh), ha)) → new_esEs9(yu300, yu40000, gh, ha)
new_esEs22(yu310, yu40010, ty_Char) → new_esEs14(yu310, yu40010)
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu301, yu40001, ty_Double) → new_esEs8(yu301, yu40001)
new_esEs20(yu301, yu40001, ty_Float) → new_esEs17(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs8(yu30, yu4000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs9(Left(yu300), Left(yu40000), ty_Float, bg) → new_esEs17(yu300, yu40000)
new_primPlusNat1(Succ(yu3400), Zero) → Succ(yu3400)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs16(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), ty_Double, bg) → new_esEs8(yu300, yu40000)
new_esEs4(yu30, yu4000, app(app(ty_@2, ca), cb)) → new_esEs12(yu30, yu4000, ca, cb)
new_esEs4(yu30, yu4000, app(app(ty_Either, bf), bg)) → new_esEs9(yu30, yu4000, bf, bg)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs24(yu301, yu40001, ty_Bool) → new_esEs10(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs15(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), ty_Integer, bg) → new_esEs15(yu300, yu40000)
new_esEs24(yu301, yu40001, app(app(app(ty_@3, bee), bef), beg)) → new_esEs13(yu301, yu40001, bee, bef, beg)
new_esEs21(yu302, yu40002, ty_Double) → new_esEs8(yu302, yu40002)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Integer) → new_esEs15(yu300, yu40000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_esEs9(Left(yu300), Left(yu40000), ty_Int, bg) → new_esEs16(yu300, yu40000)
new_esEs20(yu301, yu40001, app(app(app(ty_@3, bag), bah), bba)) → new_esEs13(yu301, yu40001, bag, bah, bba)
new_esEs17(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs16(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs19(yu300, yu40000, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs22(yu310, yu40010, ty_Integer) → new_esEs15(yu310, yu40010)
new_esEs10(False, False) → True
new_esEs21(yu302, yu40002, ty_Float) → new_esEs17(yu302, yu40002)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs19(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs22(yu310, yu40010, app(app(ty_@2, ca), cb)) → new_esEs12(yu310, yu40010, ca, cb)
new_asAs(True, yu33) → yu33
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs17(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs8(yu300, yu40000)
new_esEs11(LT, LT) → True
new_esEs4(yu30, yu4000, ty_@0) → new_esEs7(yu30, yu4000)
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs24(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs22(yu310, yu40010, ty_Double) → new_esEs8(yu310, yu40010)
new_esEs6(Nothing, Nothing, be) → True
new_esEs21(yu302, yu40002, ty_Char) → new_esEs14(yu302, yu40002)
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs9(Left(yu300), Left(yu40000), app(app(app(ty_@3, df), dg), dh), bg) → new_esEs13(yu300, yu40000, df, dg, dh)
new_esEs21(yu302, yu40002, app(ty_Maybe, bbc)) → new_esEs6(yu302, yu40002, bbc)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, ga), gb)) → new_esEs12(yu300, yu40000, ga, gb)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs26(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs24(yu301, yu40001, ty_Char) → new_esEs14(yu301, yu40001)
new_esEs6(Nothing, Just(yu40000), be) → False
new_esEs6(Just(yu300), Nothing, be) → False
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs11(GT, EQ) → False
new_esEs11(EQ, GT) → False
new_esEs24(yu301, yu40001, app(ty_Maybe, bdg)) → new_esEs6(yu301, yu40001, bdg)
new_esEs9(Left(yu300), Left(yu40000), app(ty_Ratio, ea), bg) → new_esEs18(yu300, yu40000, ea)
new_esEs21(yu302, yu40002, ty_Bool) → new_esEs10(yu302, yu40002)
new_esEs24(yu301, yu40001, app(ty_Ratio, beh)) → new_esEs18(yu301, yu40001, beh)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_Ratio, fc)) → new_esEs18(yu300, yu40000, fc)
new_esEs7(@0, @0) → True
new_esEs21(yu302, yu40002, app(app(ty_Either, bbd), bbe)) → new_esEs9(yu302, yu40002, bbd, bbe)
new_esEs12(@2(yu300, yu301), @2(yu40000, yu40001), ca, cb) → new_asAs(new_esEs23(yu300, yu40000, ca), new_esEs24(yu301, yu40001, cb))
new_esEs9(Left(yu300), Left(yu40000), app(app(ty_@2, dd), de), bg) → new_esEs12(yu300, yu40000, dd, de)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs14(yu30, yu4000)
new_esEs19(yu300, yu40000, app(ty_[], hb)) → new_esEs5(yu300, yu40000, hb)
new_esEs24(yu301, yu40001, app(app(ty_Either, bdh), bea)) → new_esEs9(yu301, yu40001, bdh, bea)
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_esEs22(yu310, yu40010, ty_Ordering) → new_esEs11(yu310, yu40010)
new_esEs9(Right(yu300), Left(yu40000), bf, bg) → False
new_esEs9(Left(yu300), Right(yu40000), bf, bg) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs21(yu302, yu40002, app(ty_Ratio, bcd)) → new_esEs18(yu302, yu40002, bcd)
new_esEs22(yu310, yu40010, ty_Int) → new_esEs16(yu310, yu40010)
new_esEs5(:(yu310, yu311), :(yu40010, yu40011), bd) → new_asAs(new_esEs22(yu310, yu40010, bd), new_esEs5(yu311, yu40011, bd))
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, gf)) → new_esEs18(yu300, yu40000, gf)

The set Q consists of the following terms:

new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Int)
new_esEs6(Just(x0), Nothing, x1)
new_esEs21(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs7(@0, @0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_[], x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Char)
new_esEs6(Nothing, Nothing, x0)
new_esEs25(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5([], [], x0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_asAs(True, x0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs5([], :(x0, x1), x2)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs19(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Ordering)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs21(x0, x1, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_esEs4(x0, x1, ty_Float)
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_esEs19(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs10(False, False)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs15(Integer(x0), Integer(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_asAs(False, x0)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs22(x0, x1, ty_Double)
new_esEs11(GT, GT)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_sr(Pos(x0), Pos(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs14(Char(x0), Char(x1))
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Ordering)
new_esEs11(LT, GT)
new_esEs11(GT, LT)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Double)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Float)
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(LT, LT)
new_esEs21(x0, x1, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Bool)
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Float)
new_primPlusNat1(Zero, Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs26(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs10(True, True)
new_esEs16(x0, x1)
new_esEs5(:(x0, x1), [], x2)
new_esEs22(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(EQ, EQ)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs24(x0, x1, app(ty_Maybe, x2))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
                    ↳ QDP
                      ↳ UsableRulesProof
QDP
                          ↳ QReductionProof
                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_lookup([], :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup([], yu41, bc, bd)

R is empty.
The set Q consists of the following terms:

new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Int)
new_esEs6(Just(x0), Nothing, x1)
new_esEs21(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs7(@0, @0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_[], x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Char)
new_esEs6(Nothing, Nothing, x0)
new_esEs25(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5([], [], x0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_asAs(True, x0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs5([], :(x0, x1), x2)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs19(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Ordering)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs21(x0, x1, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_esEs4(x0, x1, ty_Float)
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_esEs19(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs10(False, False)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs15(Integer(x0), Integer(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_asAs(False, x0)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs22(x0, x1, ty_Double)
new_esEs11(GT, GT)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_sr(Pos(x0), Pos(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs14(Char(x0), Char(x1))
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Ordering)
new_esEs11(LT, GT)
new_esEs11(GT, LT)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Double)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Float)
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(LT, LT)
new_esEs21(x0, x1, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Bool)
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Float)
new_primPlusNat1(Zero, Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs26(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs10(True, True)
new_esEs16(x0, x1)
new_esEs5(:(x0, x1), [], x2)
new_esEs22(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(EQ, EQ)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs24(x0, x1, app(ty_Maybe, x2))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Int)
new_esEs6(Just(x0), Nothing, x1)
new_esEs21(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs7(@0, @0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_[], x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Char)
new_esEs6(Nothing, Nothing, x0)
new_esEs25(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5([], [], x0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_asAs(True, x0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs5([], :(x0, x1), x2)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs19(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Ordering)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs21(x0, x1, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_esEs4(x0, x1, ty_Float)
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_esEs19(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs10(False, False)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs15(Integer(x0), Integer(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_asAs(False, x0)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs22(x0, x1, ty_Double)
new_esEs11(GT, GT)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_sr(Pos(x0), Pos(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs14(Char(x0), Char(x1))
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Ordering)
new_esEs11(LT, GT)
new_esEs11(GT, LT)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Double)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Float)
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(LT, LT)
new_esEs21(x0, x1, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Bool)
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Float)
new_primPlusNat1(Zero, Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs26(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs10(True, True)
new_esEs16(x0, x1)
new_esEs5(:(x0, x1), [], x2)
new_esEs22(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(EQ, EQ)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs24(x0, x1, app(ty_Maybe, x2))



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
                    ↳ QDP
                      ↳ UsableRulesProof
                        ↳ QDP
                          ↳ QReductionProof
QDP
                              ↳ QDPSizeChangeProof
                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_lookup([], :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup([], yu41, bc, bd)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
                    ↳ QDP
QDP
                      ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup(:(yu30, yu31), :(@2([], yu401), yu41), bc, bd) → new_lookup(:(yu30, yu31), yu41, bc, bd)
new_lookup(:(yu30, yu31), :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup1(yu30, yu31, yu4000, yu4001, yu401, yu41, new_asAs(new_esEs4(yu30, yu4000, bd), new_esEs5(yu31, yu4001, bd)), bc, bd)
new_lookup1(yu13, yu14, yu15, yu16, yu17, yu18, False, ba, bb) → new_lookup(:(yu13, yu14), yu18, ba, bb)

The TRS R consists of the following rules:

new_esEs9(Left(yu300), Left(yu40000), ty_@0, bg) → new_esEs7(yu300, yu40000)
new_primPlusNat1(Succ(yu3400), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu3400, yu40001000)))
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Ordering) → new_esEs11(yu301, yu40001)
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_esEs21(yu302, yu40002, ty_Integer) → new_esEs15(yu302, yu40002)
new_esEs4(yu30, yu4000, app(app(app(ty_@3, cc), cd), ce)) → new_esEs13(yu30, yu4000, cc, cd, ce)
new_esEs5([], [], bd) → True
new_esEs21(yu302, yu40002, ty_Ordering) → new_esEs11(yu302, yu40002)
new_esEs20(yu301, yu40001, ty_Bool) → new_esEs10(yu301, yu40001)
new_esEs9(Left(yu300), Left(yu40000), ty_Bool, bg) → new_esEs10(yu300, yu40000)
new_esEs11(EQ, EQ) → True
new_esEs23(yu300, yu40000, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs14(yu300, yu40000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs19(yu300, yu40000, app(ty_Ratio, hh)) → new_esEs18(yu300, yu40000, hh)
new_esEs18(:%(yu300, yu301), :%(yu40000, yu40001), cf) → new_asAs(new_esEs25(yu300, yu40000, cf), new_esEs26(yu301, yu40001, cf))
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs21(yu302, yu40002, app(ty_[], bbf)) → new_esEs5(yu302, yu40002, bbf)
new_esEs20(yu301, yu40001, ty_Ordering) → new_esEs11(yu301, yu40001)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_[], ee)) → new_esEs5(yu300, yu40000, ee)
new_esEs4(yu30, yu4000, app(ty_Ratio, cf)) → new_esEs18(yu30, yu4000, cf)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(ty_Either, ec), ed)) → new_esEs9(yu300, yu40000, ec, ed)
new_esEs5([], :(yu40010, yu40011), bd) → False
new_esEs5(:(yu310, yu311), [], bd) → False
new_esEs4(yu30, yu4000, app(ty_Maybe, be)) → new_esEs6(yu30, yu4000, be)
new_esEs9(Left(yu300), Left(yu40000), app(ty_Maybe, cg), bg) → new_esEs6(yu300, yu40000, cg)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs7(yu300, yu40000)
new_esEs11(GT, LT) → False
new_esEs11(LT, GT) → False
new_esEs20(yu301, yu40001, ty_Char) → new_esEs14(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(ty_@2, bda), bdb)) → new_esEs12(yu300, yu40000, bda, bdb)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs25(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs9(Left(yu300), Left(yu40000), ty_Char, bg) → new_esEs14(yu300, yu40000)
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_esEs9(Left(yu300), Left(yu40000), ty_Ordering, bg) → new_esEs11(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Float) → new_esEs17(yu301, yu40001)
new_esEs11(EQ, LT) → False
new_esEs11(LT, EQ) → False
new_esEs8(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs16(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs22(yu310, yu40010, ty_Bool) → new_esEs10(yu310, yu40010)
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), cc, cd, ce) → new_asAs(new_esEs19(yu300, yu40000, cc), new_asAs(new_esEs20(yu301, yu40001, cd), new_esEs21(yu302, yu40002, ce)))
new_esEs22(yu310, yu40010, app(ty_Maybe, be)) → new_esEs6(yu310, yu40010, be)
new_esEs15(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs11(yu30, yu4000)
new_esEs20(yu301, yu40001, app(app(ty_@2, bae), baf)) → new_esEs12(yu301, yu40001, bae, baf)
new_esEs4(yu30, yu4000, ty_Float) → new_esEs17(yu30, yu4000)
new_esEs10(True, True) → True
new_esEs20(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs22(yu310, yu40010, app(ty_Ratio, cf)) → new_esEs18(yu310, yu40010, cf)
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs22(yu310, yu40010, ty_Float) → new_esEs17(yu310, yu40010)
new_esEs4(yu30, yu4000, app(ty_[], bh)) → new_esEs5(yu30, yu4000, bh)
new_esEs20(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(ty_Either, bcf), bcg)) → new_esEs9(yu300, yu40000, bcf, bcg)
new_esEs22(yu310, yu40010, app(app(ty_Either, bf), bg)) → new_esEs9(yu310, yu40010, bf, bg)
new_esEs20(yu301, yu40001, app(ty_[], bad)) → new_esEs5(yu301, yu40001, bad)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs23(yu300, yu40000, app(ty_Ratio, bdf)) → new_esEs18(yu300, yu40000, bdf)
new_esEs19(yu300, yu40000, app(app(ty_@2, hc), hd)) → new_esEs12(yu300, yu40000, hc, hd)
new_esEs20(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_esEs26(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs19(yu300, yu40000, app(ty_Maybe, gg)) → new_esEs6(yu300, yu40000, gg)
new_esEs23(yu300, yu40000, app(ty_[], bch)) → new_esEs5(yu300, yu40000, bch)
new_esEs21(yu302, yu40002, app(app(app(ty_@3, bca), bcb), bcc)) → new_esEs13(yu302, yu40002, bca, bcb, bcc)
new_esEs25(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(ty_@2, ef), eg)) → new_esEs12(yu300, yu40000, ef, eg)
new_esEs21(yu302, yu40002, app(app(ty_@2, bbg), bbh)) → new_esEs12(yu302, yu40002, bbg, bbh)
new_esEs20(yu301, yu40001, app(ty_Ratio, bbb)) → new_esEs18(yu301, yu40001, bbb)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, gc), gd), ge)) → new_esEs13(yu300, yu40000, gc, gd, ge)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], fh)) → new_esEs5(yu300, yu40000, fh)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(app(ty_@3, eh), fa), fb)) → new_esEs13(yu300, yu40000, eh, fa, fb)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs22(yu310, yu40010, app(ty_[], bh)) → new_esEs5(yu310, yu40010, bh)
new_esEs20(yu301, yu40001, app(app(ty_Either, bab), bac)) → new_esEs9(yu301, yu40001, bab, bac)
new_esEs9(Left(yu300), Left(yu40000), app(ty_[], dc), bg) → new_esEs5(yu300, yu40000, dc)
new_esEs19(yu300, yu40000, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs24(yu301, yu40001, app(app(ty_@2, bec), bed)) → new_esEs12(yu301, yu40001, bec, bed)
new_esEs11(GT, GT) → True
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs20(yu301, yu40001, app(ty_Maybe, baa)) → new_esEs6(yu301, yu40001, baa)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs15(yu300, yu40000)
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_asAs(False, yu33) → False
new_esEs19(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_primEqNat0(Zero, Zero) → True
new_esEs19(yu300, yu40000, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_Maybe, eb)) → new_esEs6(yu300, yu40000, eb)
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_esEs19(yu300, yu40000, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, fd)) → new_esEs6(yu300, yu40000, fd)
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs10(yu30, yu4000)
new_esEs21(yu302, yu40002, ty_Int) → new_esEs16(yu302, yu40002)
new_esEs19(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs13(yu300, yu40000, bdc, bdd, bde)
new_esEs22(yu310, yu40010, app(app(app(ty_@3, cc), cd), ce)) → new_esEs13(yu310, yu40010, cc, cd, ce)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs16(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), app(app(ty_Either, da), db), bg) → new_esEs9(yu300, yu40000, da, db)
new_esEs23(yu300, yu40000, app(ty_Maybe, bce)) → new_esEs6(yu300, yu40000, bce)
new_esEs19(yu300, yu40000, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs21(yu302, yu40002, ty_@0) → new_esEs7(yu302, yu40002)
new_esEs24(yu301, yu40001, app(ty_[], beb)) → new_esEs5(yu301, yu40001, beb)
new_esEs22(yu310, yu40010, ty_@0) → new_esEs7(yu310, yu40010)
new_primPlusNat0(Succ(yu340), yu4000100) → Succ(Succ(new_primPlusNat1(yu340, yu4000100)))
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs20(yu301, yu40001, ty_Double) → new_esEs8(yu301, yu40001)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, ff), fg)) → new_esEs9(yu300, yu40000, ff, fg)
new_esEs19(yu300, yu40000, app(app(app(ty_@3, he), hf), hg)) → new_esEs13(yu300, yu40000, he, hf, hg)
new_esEs14(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs19(yu300, yu40000, app(app(ty_Either, gh), ha)) → new_esEs9(yu300, yu40000, gh, ha)
new_esEs22(yu310, yu40010, ty_Char) → new_esEs14(yu310, yu40010)
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu301, yu40001, ty_Double) → new_esEs8(yu301, yu40001)
new_esEs20(yu301, yu40001, ty_Float) → new_esEs17(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs8(yu30, yu4000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs9(Left(yu300), Left(yu40000), ty_Float, bg) → new_esEs17(yu300, yu40000)
new_primPlusNat1(Succ(yu3400), Zero) → Succ(yu3400)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs16(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), ty_Double, bg) → new_esEs8(yu300, yu40000)
new_esEs4(yu30, yu4000, app(app(ty_@2, ca), cb)) → new_esEs12(yu30, yu4000, ca, cb)
new_esEs4(yu30, yu4000, app(app(ty_Either, bf), bg)) → new_esEs9(yu30, yu4000, bf, bg)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs24(yu301, yu40001, ty_Bool) → new_esEs10(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs15(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), ty_Integer, bg) → new_esEs15(yu300, yu40000)
new_esEs24(yu301, yu40001, app(app(app(ty_@3, bee), bef), beg)) → new_esEs13(yu301, yu40001, bee, bef, beg)
new_esEs21(yu302, yu40002, ty_Double) → new_esEs8(yu302, yu40002)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Integer) → new_esEs15(yu300, yu40000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_esEs9(Left(yu300), Left(yu40000), ty_Int, bg) → new_esEs16(yu300, yu40000)
new_esEs20(yu301, yu40001, app(app(app(ty_@3, bag), bah), bba)) → new_esEs13(yu301, yu40001, bag, bah, bba)
new_esEs17(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs16(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs19(yu300, yu40000, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs22(yu310, yu40010, ty_Integer) → new_esEs15(yu310, yu40010)
new_esEs10(False, False) → True
new_esEs21(yu302, yu40002, ty_Float) → new_esEs17(yu302, yu40002)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs19(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs22(yu310, yu40010, app(app(ty_@2, ca), cb)) → new_esEs12(yu310, yu40010, ca, cb)
new_asAs(True, yu33) → yu33
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs17(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs8(yu300, yu40000)
new_esEs11(LT, LT) → True
new_esEs4(yu30, yu4000, ty_@0) → new_esEs7(yu30, yu4000)
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs24(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs22(yu310, yu40010, ty_Double) → new_esEs8(yu310, yu40010)
new_esEs6(Nothing, Nothing, be) → True
new_esEs21(yu302, yu40002, ty_Char) → new_esEs14(yu302, yu40002)
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs9(Left(yu300), Left(yu40000), app(app(app(ty_@3, df), dg), dh), bg) → new_esEs13(yu300, yu40000, df, dg, dh)
new_esEs21(yu302, yu40002, app(ty_Maybe, bbc)) → new_esEs6(yu302, yu40002, bbc)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, ga), gb)) → new_esEs12(yu300, yu40000, ga, gb)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs26(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs24(yu301, yu40001, ty_Char) → new_esEs14(yu301, yu40001)
new_esEs6(Nothing, Just(yu40000), be) → False
new_esEs6(Just(yu300), Nothing, be) → False
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs11(GT, EQ) → False
new_esEs11(EQ, GT) → False
new_esEs24(yu301, yu40001, app(ty_Maybe, bdg)) → new_esEs6(yu301, yu40001, bdg)
new_esEs9(Left(yu300), Left(yu40000), app(ty_Ratio, ea), bg) → new_esEs18(yu300, yu40000, ea)
new_esEs21(yu302, yu40002, ty_Bool) → new_esEs10(yu302, yu40002)
new_esEs24(yu301, yu40001, app(ty_Ratio, beh)) → new_esEs18(yu301, yu40001, beh)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_Ratio, fc)) → new_esEs18(yu300, yu40000, fc)
new_esEs7(@0, @0) → True
new_esEs21(yu302, yu40002, app(app(ty_Either, bbd), bbe)) → new_esEs9(yu302, yu40002, bbd, bbe)
new_esEs12(@2(yu300, yu301), @2(yu40000, yu40001), ca, cb) → new_asAs(new_esEs23(yu300, yu40000, ca), new_esEs24(yu301, yu40001, cb))
new_esEs9(Left(yu300), Left(yu40000), app(app(ty_@2, dd), de), bg) → new_esEs12(yu300, yu40000, dd, de)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs14(yu30, yu4000)
new_esEs19(yu300, yu40000, app(ty_[], hb)) → new_esEs5(yu300, yu40000, hb)
new_esEs24(yu301, yu40001, app(app(ty_Either, bdh), bea)) → new_esEs9(yu301, yu40001, bdh, bea)
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_esEs22(yu310, yu40010, ty_Ordering) → new_esEs11(yu310, yu40010)
new_esEs9(Right(yu300), Left(yu40000), bf, bg) → False
new_esEs9(Left(yu300), Right(yu40000), bf, bg) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs21(yu302, yu40002, app(ty_Ratio, bcd)) → new_esEs18(yu302, yu40002, bcd)
new_esEs22(yu310, yu40010, ty_Int) → new_esEs16(yu310, yu40010)
new_esEs5(:(yu310, yu311), :(yu40010, yu40011), bd) → new_asAs(new_esEs22(yu310, yu40010, bd), new_esEs5(yu311, yu40011, bd))
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, gf)) → new_esEs18(yu300, yu40000, gf)

The set Q consists of the following terms:

new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Int)
new_esEs6(Just(x0), Nothing, x1)
new_esEs21(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs7(@0, @0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_[], x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Char)
new_esEs6(Nothing, Nothing, x0)
new_esEs25(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5([], [], x0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_asAs(True, x0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs5([], :(x0, x1), x2)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs19(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Ordering)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs21(x0, x1, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_esEs4(x0, x1, ty_Float)
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_esEs19(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs10(False, False)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs15(Integer(x0), Integer(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_asAs(False, x0)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs22(x0, x1, ty_Double)
new_esEs11(GT, GT)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_sr(Pos(x0), Pos(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs14(Char(x0), Char(x1))
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Ordering)
new_esEs11(LT, GT)
new_esEs11(GT, LT)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Double)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Float)
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(LT, LT)
new_esEs21(x0, x1, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Bool)
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Float)
new_primPlusNat1(Zero, Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs26(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs10(True, True)
new_esEs16(x0, x1)
new_esEs5(:(x0, x1), [], x2)
new_esEs22(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(EQ, EQ)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs24(x0, x1, app(ty_Maybe, x2))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: